\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $A$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$), $n$:$\mathbb{N}$,\+
\\[0ex]$L$:event{-}info(${\it ds}$;${\it da}$) List, $k$:Knd, $s$:State(${\it ds}$), $v$:Valtype(${\it da}$;$k$).
\-\\[0ex]ecl{-}trans{-}act(${\it ds}$;${\it da}$;$A$)($n$,$L$ @ [$\langle$$k$$,\,$$s$$,\,$$v$$\rangle$])
\\[0ex]$\Leftrightarrow$
\\[0ex]($k$ $\in$ ecl{-}trans{-}ks($A$)) \& ecl{-}trans{-}a($A$)($n$,$k$,$s$,$v$,ecl{-}trans{-}state($A$;$L$))
\end{tabbing}